r:Rng, e:|r|, a, b:. ((a+b) r e) = ((a r e) +r (b r e))  |r| 

latex

Definitions	t  T, IMonoid, x f y, x:A. B(x), t.2, t.1, , P & Q, Mon, Group{i}, AbGrp, r+gp, *, |g|, n r e
Lemmas	rng wf, abgrp wf, grp id wf, grp op wf, grp car wf, monoid p wf, add grp of rng wf b, mon nat op add